Nuprl Definition : ecl-trans-act
0,22
postcript
pdf
ecl-trans-act(
ds
;
da
;
A
)(
n
,
L
)
==
L'
:event-info(
ds
;
da
) List,
tr
:event-info(
ds
;
da
).
==
L
= (
L'
@ [
tr
])
==
& let
k
,
s
,
v
=
tr
in (
k
ecl-trans-ks(
A
)) & ecl-trans-a(
A
)(
n
,
k
,
s
,
v
,ecl-trans-state(
A
;
L'
))
latex
clarification:
ecl-trans-act(
ds
;
da
;
A
)(
n
,
L
)
==
L'
:event-info(
ds
;
da
) List,
tr
:event-info(
ds
;
da
).
==
L
= (
L'
@ (
tr
.nil))
event-info(
ds
;
da
) List
==
& let
k
,
s
,
v
=
tr
in
== &
(
k
ecl-trans-ks(
A
)
Knd) & ecl-trans-a(
A
)(
n
,
k
,
s
,
v
,ecl-trans-state(
A
;
L'
))
latex
Definitions
x
:
A
.
B
(
x
)
,
P
&
Q
,
event-info(
ds
;
da
)
,
as
@
bs
,
let
x
,
y
,
z
=
a
in
t
(
x
;
y
;
z
)
,
A
&
B
,
(
x
l
)
,
ecl-trans-ks(
v
)
,
Knd
,
b
,
ecl-trans-a(
v
)
,
ecl-trans-state(
v
;
L
)
FDL editor aliases
ecl-trans-act
origin